Nuprl Lemma : glued-Q-R-glued 11,40
es:ES, A, B:Type, Ia:AbsInterface(A), Ib:AbsInterface(B), f:(E(Ia)B).
glued(es; B; f; Ia; Ib)
 Q-R-glued(es; B; f; Ia; (e,e'. e loc e' ); Ib; (e,e'. e loc e' )) 
latex

Definitionsglues(es; B; g; f; Ia; Ib), x:A. B(x), x:A  B(x), glued(es; B; f; Ia; Ib), Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), e loc e' , g glues Ia:Qa f Ib:Rb, f(a), EState(T), Id, , x:AB(x), t  T, x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, s = t, b, A, P  Q, constant_function(f;A;B), Type, kindcase(k; a.f(a); l,t.g(l;t) ), Knd, P & Q, Top, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, left + right, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), ES, AbsInterface(A), E(X), P  Q, P  Q
Lemmases-E-interface wf, val-axiom wf, constant function wf

origin